Nuprl Lemma : tree_con_wf
4,23
postcript
pdf
E
,
T
:Type. tree_con(
E
;
T
)
Type
latex
Definitions
tree_con(
E
;
T
)
,
x
:
A
.
B
(
x
)
,
t
T
origin
E, T:Type. tree_con(E;T) 
Type E, T:Type. tree_con(E;T) Type x:A. B(x) T